COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDVAR x y z ε REAL
C00004 ENDMK
C⊗;
declare INDVAR x y z ε REAL;
declare OPCONST pred(REAL) = REAL[PRE];
declare OPCONST tak0(REAL,REAL,REAL) = REAL;
declare OPCONST tak1(REAL,REAL,REAL) = REAL;
declare PREDCONST <(REAL,REAL)[L←455,R←455];
declare PREDCONST ≤(REAL,REAL)[L←455,R←455];

AXIOM LESS:
	∀x.(pred(x) < x)
	∀x.(pred(x) ≤ x)
	∀x y.((x < y ∧ ¬x=y ∧ ¬(y<x)) ∨ (¬(x<y)∧x=y∧¬(y<x)) ∨ (¬(x<y)∧¬x=y∧y<x))
	∀x y z.((x<y ∧ y<z ⊃ x<z) ∧ (x≤y ∧ y<z ⊃ x<z) ∧ (x<y ∧ y≤z ⊃ x<z)
∧ (x≤y ∧ y≤z ⊃ x≤z))
	∀x y.(x≤y ≡ x<y ∨ x=y)
	∀x.¬(x < x)
	∀x.x≤x
	∀x y.(¬(x≤y) ≡ y < x)
	∀x y.(y < x ≡ ¬(x≤y))
;;

AXIOM TAK0:
	∀x y z.(tak0(x,y,z) = IF x≤y THEN y ELSE (IF y≤z THEN z ELSE x));;
AXIOM TAK1:
	∀x y z.(tak1(x,y,z) = IF x≤y THEN y ELSE tak0(tak0(pred x,y,z),
tak0(pred y,z,x),tak0(pred z,x,y)));;